theory GPTEE_DataStructure

imports Main 
begin
section "DEFINITION"
type_synonym SYSTEM_TIME_TYPE = nat
type_synonym TEE_UUID_TYPE = nat
type_synonym TA_UUID_TYPE = nat
type_synonym CANCEL_TYPE = bool 
type_synonym TIMEOUT_TYPE = nat
type_synonym TEE_PARAM_TYPES_TYPE = int
type_synonym BUFFER_OFFSET_TYPE = nat
type_synonym REF_MEM_OFFSET_TYPE = int
type_synonym COMMAND_ID_TYPE = nat
type_synonym TEE_DRIVER_TYPE = int
type_synonym SHM_FLAG_TYPE = bool
type_synonym SESSION_ID_TYPE = nat
type_synonym MULTI_SESSION_TYPE = bool
type_synonym INSTANCE_KEEP_ALIVE_TYPE = bool
type_synonym SINGLE_INSTANCE_TYPE = bool
type_synonym TEEC_VALUE_TYPE = nat
type_synonym UINT32_t = int
type_synonym FD_TYPE = nat
type_synonym REF_CNT_TYPE = nat
type_synonym BUSY_TYPE = bool
type_synonym THREAD_ID_TYPE = nat
type_synonym TIME_OFFSET_TYPE = nat
type_synonym TA_PRIORITY_TYPE = nat
type_synonym TEE_RESULT = nat
type_synonym BUFFER_ID_TYPE = nat
type_synonym BUFFER_SIZE_TYPE = nat
type_synonym VMO_ID_TYPE = nat
type_synonym VMO_SIZE_TYPE = nat
datatype TA_MODE_TYPE = DEAD | COLD_START | NORMAL
type_synonym INIT = bool
type_synonym OFFSET = nat
type_synonym DOMAIN_ID = nat
type_synonym SYSTIME = nat
type_synonym CHECKCODE = nat
type_synonym Connection_Method = nat
type_synonym Connection_Data = string
type_synonym MEM_BLOCK_ID = nat
type_synonym TOTAL_SIZE = nat
type_synonym BIN_MEM_SIZE = nat
type_synonym TEE_OWN_SIZE = nat

(*added 2023.2.24 for load TA service*)
type_synonym MESSAGE_HEAD_TYPE = nat
type_synonym BIN_TYPE = nat
type_synonym SIG_VER = nat
type_synonym ALGO = nat
type_synonym IMG_TYPE = nat
type_synonym RESV = nat
type_synonym RAW_IMG_SIZE = nat
type_synonym RAWING_HASH = nat
type_synonym IMG_HASH = nat
type_synonym SIG = nat
type_synonym BIN_BODY = nat
record BIN =
    message_head :: "MESSAGE_HEAD_TYPE"
    bin_result :: "BIN_TYPE"
    sig_ver :: "SIG_VER"
    algo :: "ALGO"
    img_type :: "IMG_TYPE"
    resv :: "RESV"
    raw_img_size :: "RAW_IMG_SIZE"
    rawing_hash :: "RAWING_HASH"
    img_hash :: "IMG_HASH"
    sig :: "SIG"
    bin_body :: "BIN_BODY"  (* stand for binary code of ta *)


(*size of TA bin, should get from bin but here only set to be an constant*)
consts bin_mem_size::"BIN_MEM_SIZE"
consts tee_own_size::"TEE_OWN_SIZE"
consts someblockID1::nat
consts someblockID2::nat


definition INVALID_SESSION_ID where
        "INVALID_SESSION_ID ≡(0::SESSION_ID_TYPE)"


datatype accessFlags = TEE_MEMORY_ACCESS_ANY_OWNER 
  | TEE_MEMORY_ACCESS_SECURE  | TEE_MEMORY_ACCESS_NONSECURE  | TEE_MEMORY_ACCESS_WRITE
  | TEE_MEMORY_ACCESS_READ

datatype hint = TEE_MALLOC_FILL_ZERO  |  TEE_USER_MEM_HINT_NO_FILL_ZERO

datatype RIGHT_TYPE=TA_PERMISSION_GET_HWINFO|TA_PERMISSION_ACCESS_MISC_DEV|TA_PERMISSION_ACCESS_PLATFORM|TA_PERMISSION_ACCESS_SPI

record RIGHT = 
      hwinfo::RIGHT_TYPE
      misc_dev::RIGHT_TYPE
      access_platform::RIGHT_TYPE
      access_api::RIGHT_TYPE

datatype TEE_RETURN_CODE_TYPE = TEE_SUCCESS 
  | TEE_PARAM_TYPE_NONE | TEE_PARAM_TYPE_VALUE_INPUT | TEE_PARAM_TYPE_MEMREF_INPUT
  | TEE_PARAM_TYPE_VALUE_OUTPUT | TEE_PARAM_TYPE_MEMREF_OUTPUT | TEE_PARAM_TYPE_MEMREF_INOUT
  | TEE_ERROR_OUT_OF_MEMORY | TEE_ERROR_ITEM_NOT_FOUND | TEE_ERROR_ACCESS_CONFLICT
  | TEE_ERROR_BUSY | TEE_ERROR_TARGET_DEAD | TEE_ERROR_CANCEL | TEE_ERROR_BAD_PARAMETERS 
  | TEE_ERROR_SECURITY | TEE_ERROR_BAD_STATE | TEE_ERROR_GENERIC


datatype TEEC_RETURN_CODE_TYPE = TEEC_SUCCESS 
  | TEEC_ERROR_BAD_PARAMETERS |TEEC_ERROR_ITEM_NOT_FOUND|TEEC_ERROR_SECURITY|TEEC_ERROR_BUSY| TEEC_ERROR_OUT_OF_MEMORY

datatype TEEC_RET_ORIGIN = TEEC_ORIGIN_API|TEEC_ORIGIN_COMMS|TEEC_ORIGIN_TEE|TEEC_ORIGIN_TRUSTED_APP

(*name should be a string but cant express in Isabelle, so change to nat*)
type_synonym TEE_NAME = nat(*used in TEEC_initializeContext*)
type_synonym TEEC_RESULT = TEEC_RETURN_CODE_TYPE

datatype FLAGS_TYPE = TEEC_MEM_INPUT | TEEC_MEM_OUTPUT

datatype MEM_RIGHT = READ|WRITE|READWRITE

(*describe the param type of input shared memory in openSession and invokeCommand*)
datatype TEEC_MEMREF_TYPE = TEEC_MEMREF_PARTIAL_INPUT | TEEC_MEMREF_PARTIAL_OUTPUT | 
                       TEEC_MEMREF_PARTIAL_INOUT

datatype TEE_MEMREF_TYPE = TEE_MEMREF_PARTIAL_INPUT | TEE_MEMREF_PARTIAL_OUTPUT | 
                       TEE_MEMREF_PARTIAL_INOUT


                

(*only parameters used in registersharedmemory, not real memblock*)
record TEEC_SharedMemory =
  buffer :: MEM_BLOCK_ID
  shared_size :: BUFFER_SIZE_TYPE
  flags :: FLAGS_TYPE
  (*TEEC_MEM_INPUT or TEEC_MEM_OUTPUT*)
  shared_id :: BUFFER_ID_TYPE
  alloced_size :: BUFFER_SIZE_TYPE
  shadow_buffer :: MEM_BLOCK_ID
  registered_fd :: FD_TYPE
  buffer_allocated :: bool

(*a memory block whose size is adjustable*)

(*we have four memory types: TA, TA bin, REE, TEE, only TA bin can be accessed by TA and TEE*)
record MemBlock = 
          block_id :: MEM_BLOCK_ID
          size :: nat
          ownership :: DOMAIN_ID
          access_right :: "DOMAIN_ID ⇀ MEM_RIGHT"
          is_SecureMem :: bool (*secure means belong to TEE, else REE*)
          related::"MEM_BLOCK_ID option"
          

(*
  TEEC_Parameter: Memory container to be used when passing data between
      client application and trusted code.
      Either the client uses a shared memory reference, parts of it or a small raw data container.
  (1)tmpref: A temporary memory reference only valid for the duration of the operation.
  (2)memref: The entire shared memory or parts of it.
  (3)value: The small raw data container to use 
*)

(*
record TEEC_PARAMETER = 
  tmpref :: "TEEC_TempMemoryReference_TYPE"
  memref :: "TEEC_RegisteredMemoryReference"
  teec_value :: "TEEC_Value" 
*)

(*
datatype TEE_PARAM_TYPE = TEEC_NONE | TEEC_VALUE | tmt TEEC_MEMREF_TEMP | TEEC_MEMREF_WHOLE | TEEC_MEMREF_PARTIAL
*)


(*
  [Constant Name]              |  [Equivalent on Client API]
  TEE_PARAM_TYPE_NONE          |  TEEC_NONE
  TEE_PARAM_TYPE_VALUE_INPUT   |  TEEC_VALUE_INPUT
  TEE_PARAM_TYPE_VALUE_OUTPUT  |  TEEC_VALUE_OUTPUT
  TEE_PARAM_TYPE_VALUE_INOUT   |  TEEC_VALUE_INOUT
  TEE_PARAM_TYPE_MEMREF_INPUT  |  TEEC_MEMREF_TEMP_INPUT or TEEC_MEMREF_PARTIAL_INPUT
  TEE_PARAM_TYPE_MEMREF_OUTPUT |  TEEC_MEMREF_TEMP_OUTPUT or TEEC_MEMREF_PARTIAL_OUTPUT
  TEE_PARAM_TYPE_MEMREF_INOUT  |  TEEC_MEMREF_TEMP_INOUT or TEEC_MEMREF_PARTIAL_INOUT
*)
datatype TEE_PARAM_TYPE = TEE_PARAM_TYPE_NONE | TEE_PARAM_TYPE_VALUE | tmt MemBlock


record PARAMS_TYPE =
   paramTypes :: "TEE_PARAM_TYPES_TYPE list"
   paramsVal :: "TEE_PARAM_TYPE list"
  

(* TEE_RETURN_ORIGIN_TYPE: a pointer to a variable which will contain the return origin. This field may be NULL if the return origin is not needed. *)
datatype TEE_RETURN_ORIGIN_TYPE = TEE_ORIGIN_API | TEE_ORIGIN_COMMS | TEE_ORIGIN_TEE | TEE_ORIGIN_TRUSTED_APP

datatype LOGIN_TYPE = REE_PUBLIC | TRUSTED_APP |KERN_IDENTITY|DTC_IDENTITY
(*12.29: kern and dtc are for TEE,ree means nsapp*)

(* 
  driver_fd: TEE driver file
  reg_mem : if TEE support dynamic shared mem then reg_mem = true 

record TEEC_CONTEXT_TYPE = 
  driver_fd :: TEE_DRIVER_TYPE
  reg_mem :: SHM_FLAG_TYPE
*)

(*
  TEEC_Operation: Holds information and memory references used in TEEC_InvokeCommand()/TEEC_OpenSession().
  (1)started: Client must initialize to zero if it needs to cancel
           an operation about to be performed.
  (2)paramTypes paramsVal: params
  (3)session: Internal pointer to the last session used by TEEC_InvokeCommand with this operation.
*)


record TEEC_Operation = 
  started :: "UINT32_t"
  paramTypes :: "TEE_PARAM_TYPES_TYPE list"
  paramsVal :: "TEE_PARAM_TYPE list"
 (* session :: TEEC_SESSION_TYPE*)



(*client_id*)
record CLIENT_TYPE =
  login :: LOGIN_TYPE
  id :: "TA_UUID_TYPE option"

definition DefaultClientID where "DefaultClientID ≡ ⦇login=REE_PUBLIC,id=None⦈"

definition DefaultThreadID where "DefaultThreadID ≡ 0::nat"


(*
(*including KERN and DTC, and NDSPP is REE whose login is REE_PUBLIC *)
definition KERN_IDENTITY where
      "KERN_IDENTITY ≡ ⦇ login = TRUSTED_APP,
        id = Some (1::nat)⦈ 
      "
*)


subsection "PARAMETER for Mid functions"





subsection "TEE model params"

(*
  TEEC_Parameter: Memory container to be used when passing data between
      client application and trusted code.
      Either the client uses a shared memory reference, parts of it or a small raw data container.
  (1)tmpref: A temporary memory reference only valid for the duration of the operation.
  (2)memref: The entire shared memory or parts of it.
  (3)value: The small raw data container to use 
*)


record TEE_Memref = 
  paramTypes :: "TEE_PARAM_TYPES_TYPE list"
  paramsVal :: "TEE_PARAM_TYPE list"



typedecl TEE_TASessionHandle

(*
record VMO_ATTR_TYPE =
  size :: VMO_SIZE_TYPE
  id :: VMO_ID_TYPE
*)

(*-----------------------------------------------------------------------------------*)
section "MITEE MODEL"          
subsection "REE model"


(*
  TEEC_CONTEXT_TYPE: i.e. TEEC_context, only as parameter, for CA
  driver_fd: ca node fd
  reg_mem: if TEE support dynamic shared mem
*)
record TEEC_CONTEXT_TYPE = 
  ca_fd :: FD_TYPE
  reg_mem :: SHM_FLAG_TYPE

(*1.1.1 tee_ctx list in REE, designed for driver*)
record TEE_CONTEXT_TYPE = 
    ctx_fd :: FD_TYPE
    tee_reg_mem :: SHM_FLAG_TYPE
    driver_session_list :: "SESSION_ID_TYPE list"
   (* lst_mem :: "MEM_BLOCK_ID list"*)


(* 
TEEC_SESSION_TYPE means session between CA and TA
ctx : logic connection between client and TEE
session_id : identify a ta session between CA and TA
*)

(*TBD*)
record TEEC_SESSION_TYPE = 
  teec_ctx :: TEEC_CONTEXT_TYPE
  teec_session_id :: SESSION_ID_TYPE




record REE_TYPE = 
  driver_mem :: "MemBlock list"
  tee_ctx_list :: "TEE_CONTEXT_TYPE list"
  ree_total_size :: TOTAL_SIZE


subsection "TA model"
record TEE_TA_ATTR_TYPE = 
  multiSession :: MULTI_SESSION_TYPE
  keepAlive :: INSTANCE_KEEP_ALIVE_TYPE
  singleInstance :: SINGLE_INSTANCE_TYPE

(*
  TEE_TA_TYPE: TA type in TAs

record TEE_TA_TYPE =
  ta_session_list :: "SESSION_ID_TYPE list"
  attribute :: TEE_TA_ATTR_TYPE
  ta_mem :: "TEEC_SharedMemory_TYPE list"
  ta_right :: RIGHT
  ta_init :: INIT 
(*when openSession check if INIT is false, if so,set true and execute TA_CreateEntryPoint*)
*)


subsection "TEE model"
(*TA Instance list in TA-mgr*)
(* add ta_cur_session_id  *)
record TA_INSTANCE_CTX_TYPE=
  ta_id :: TA_UUID_TYPE
  cur_ta_session_list :: "SESSION_ID_TYPE list" (* cur TA is the client side of the session in the session id list *)
  reference_cnt :: REF_CNT_TYPE
  busy :: BUSY_TYPE
  cur_ta_thread_id :: THREAD_ID_TYPE
  attribute :: TEE_TA_ATTR_TYPE
 (* ta_cur_session_id :: SESSION_ID_TYPE *) (*not used in function logic*)
 (* panicked :: bool *) (*not used in function logic*)


(*2.2.1 sesssion list in TA-mgr*)
record TA_MGR_SESSION_TYPE = 
  session_id :: SESSION_ID_TYPE
  session_ctx :: THREAD_ID_TYPE (*use thread id as a only pointer to ctx, uuid cant deal with multiInstance*)
                                 (*this tid belongs to server TA*)
  client_id :: CLIENT_TYPE


record TEE_TA_MANAGER =
  mgr_ta_sessions :: "TA_MGR_SESSION_TYPE list"
  mgr_ta_instances :: "TA_INSTANCE_CTX_TYPE list"
  BIDpointer :: nat (*the pointer for allocation of mem block id on TEE side
                      , plus one after allocate once*)
  (*createdVmo :: "TEE_UUID_TYPE × VMO_ID_TYPE ⇀ VMO_ATTR_TYPE"*)
  (*TBD*)


record ZIRCON_TYPE =  
  property :: "TA_UUID_TYPE ⇀ TA_PRIORITY_TYPE"
(*TBD*)


(*
  TEE/REE IPC DRIVER_TYPE
*)
type_synonym TEE_REE_IPC_DRIVER_TYPE=nat

record TEE_TYPE = 
  ta_mgr :: TEE_TA_MANAGER
  tee_ree_ipc_driver :: TEE_REE_IPC_DRIVER_TYPE
  zircon :: ZIRCON_TYPE
  tee_memories :: "MemBlock list"
  tee_total_size :: TOTAL_SIZE



section "State and Configuration" 

record BIN_Handle =
    mem_block :: "MemBlock option"
    tabin :: "BIN option"

consts binHandle::"BIN_Handle option"



(*datatype TA_CONF = TAConf TA_UUID_TYPE "SESSION list" TEE_TA_ATTR_TYPE "MEM_BLOCK_ID list" RIGHT INIT OFFSET BIN*)
datatype TA_CONF = TAConf TA_UUID_TYPE  TEE_TA_ATTR_TYPE RIGHT INIT OFFSET BIN
type_synonym TAs = "TA_UUID_TYPE⇀TA_CONF"

(*basic system configuration of GP TEE*)
record Sys_Config = 
                    REE :: DOMAIN_ID 
                    TEE :: DOMAIN_ID
                    TA_conf :: TAs
                    checkcode :: CHECKCODE
                    TEE_name :: TEE_NAME
                    DefaultREESize :: TOTAL_SIZE
                    DefaultTEESize :: TOTAL_SIZE
          

record TA_State_Type = 
                TA_mode :: TA_MODE_TYPE
                TA_sessions :: "SESSION_ID_TYPE list" (* cur TA is the server side of the session in the session id list *)
               (* TA_memories :: "MemBlock list" *)
                TA_instance_init :: INIT
                TA_attribute :: TEE_TA_ATTR_TYPE
                

type_synonym TAs_State = "THREAD_ID_TYPE⇀TA_State_Type"



record EVENT_PARAM =
                   param1::"nat option"
                   param2::"nat option"
                   param3::"TEEC_Operation option"
                   param4::"CLIENT_TYPE option"
                   param5::"TEEC_CONTEXT_TYPE option"
                   param6::"nat option"
                   param7::"PARAMS_TYPE option"
                   param8::"PARAMS_TYPE option"
                   param9::"TA_INSTANCE_CTX_TYPE option"
                   param10::"MemBlock option"(*12.18 added*)
                   param11::"TEEC_MEMREF_TYPE option"(*12.18 added*)
                   param12::"TEEC_RETURN_CODE_TYPE option"(*1.5 added*)
                   param13::"TEE_RETURN_CODE_TYPE option" (*1.5 added*)

datatype EVENT_NAME = TEEC_OP1|TEEC_OP2|TEEC_OP3|TEEC_OP4|TEE_OP1|TEE_OP2|TEE_OP3|TEE_OP4|TEE_IC1|TEE_IC2|TEE_IC3|TEE_IC4
                      |TEE_CS1|TEE_CS2|TEE_CS3|TEE_CS4|TEEC_IC1|TEEC_IC2|TEEC_IC3|TEEC_IC4|TEEC_CS1|TEEC_CS2|TEEC_CS3|TEEC_CS4
(*designed for exec_prime in s,  prime is a list of events which should be executed first,e.g.,after
OpenSession, a tuple was added, after EVENT_NAME execute successfully, that tuple was deleted*)



(*Global system state of GP TEE*)
record State = 
        current :: DOMAIN_ID
        TAs_state :: TAs_State
        REE_state :: REE_TYPE
        TEE_state :: TEE_TYPE
        system_time :: SYSTIME
        exec_prime :: "(EVENT_PARAM × EVENT_NAME) list"
(**)

end